#include <vector>
#include <string>
#include <stdint.h>
#include <map>
#include <utility>
#include <sstream>
#include <sys/time.h>//debug

#ifndef DIVINE_SYMBOLICS_H
#define DIVINE_SYMBOLICS_H

namespace divine {

const uint32_t bit_width = 4;//shouldn't be const, but for now...
const uint32_t distinct_inports = 0; //set to zero for full verification
const uint32_t distinct_invalues = 1; 

//just two functions to ease reading and writing to blobs
template< typename Out >
void blobRead( Out *o, char **i ) {
  *o = *reinterpret_cast< Out* >( *i );
  *i += sizeof( Out );
}

template< typename In >
void blobWrite( char **o, In *i ) {
  *reinterpret_cast< In* >( *o ) = *i;
  *o += sizeof( In );
}

//some basic types for abstract syntax trees (AST)
enum TYPE {VAR, CON, OP};
  
enum OPTYPE {NOT, AND, OR, XOR, NAND, NOR, IMP,
             PLUS, TIMES, POW, SQRT, MIN, MAX,
             LT, LE, GT, GE, NEQ, EQ,
             CEIL, FLOOR, ROUND, FIX, //are we ready for floats?
             CAST, SWITCH, MSWITCH, BEET, ABS};

//ahead declaration - contains original expressions and real names
struct SMTRep;

//node in AST
struct Node {
  TYPE type;
  OPTYPE op; //if operator
  int arity; //if operator
  int name; //if variable
  int round; //Simulink speciality - every tick has new variables
  uint32_t value; //if constant
  //successors are indices into a vector, not pointers
  std::vector< uint32_t > heirs;

  Node();
  Node( int );
  Node( const Node& );
  Node( TYPE, OPTYPE, int, uint32_t, uint32_t );
  Node( TYPE, uint32_t );

  int size();
  void rebuild( char** );
  void store( char** );
  void print( std::string );
};

//AST expression is a vector of nodes, root is node on index 0
//node is either a leaf (arity 0) or an inner node (arity >0)
//inner nodes have explicitly stored the indices of their successors
//parsing is easy but building is a pain; may not be very efficient
struct Expr {
  std::vector< Node > nodes;
  uint32_t root; //never used, just for creating new expressions
  SMTRep *smt;//reference for real names of variables, and other stuff

  Expr() {}
  Expr( SMTRep *);
  Expr( Expr & );
  Expr( const Expr & );
  Expr( Expr * );
  
  bool check_sanity();
  void round( int );
  void subs( int, Expr * );

  std::string convert( uint32_t, bool );
  std::string convert( std::string, bool );
  std::string translate( bool, std::string );
  std::string tran( uint32_t, bool, std::string );
  std::string print();
  
  void clear();
  int size();
  void rebuild( char** );
  void store( char** );
};

//simple type for identifying Simulink variable types
enum ID { DEL, OUT, INP };

//mediates communication between DiVinE and SMT solver
struct SMTRep
{
  //information on original Simulink variables
  struct NFO {
    Expr e;
    std::string s;
    ID d;

    NFO( Expr _e, std::string _s, ID _d ): e( _e ), s( _s ), d( _d ) {}
  };
  
  std::vector< NFO > os; //all we need from the original diagram
  std::vector< uint32_t > in_values; //for counterexample
  //state is represented by pcs only
  //pc contains one expression for every round (tick)
  std::vector< Expr > pc;

  bool cond_tick; //helper Boolean, see definition of tick() and pc_sat()
  int offset; //sometimes we need to read blobs directly

  //debug stuff
  timeval timer;
  int counter;
  void startTimer() { gettimeofday( &timer, NULL ); }
  uint32_t endTimer() {
    timeval tmp;
		gettimeofday( &tmp, NULL );
		tmp.tv_sec -= timer.tv_sec;
		tmp.tv_usec -= timer.tv_usec;
		if ( tmp.tv_usec < 0 ) {
				tmp.tv_usec += 1000000;
				tmp.tv_sec--;
		}
		return uint32_t( (tmp.tv_usec + tmp.tv_sec * 1000000) / 1000 );
  }
  struct Report {
    uint32_t checks;
    uint32_t time;
    uint32_t size;
    uint32_t state_size;
    uint32_t assertions;
  };
  std::vector< Report > times;
  //debug stuff

  SMTRep();
  SMTRep( SMTRep * );
  
  void tick();
  int size();
  
  std::string convert( uint32_t, bool );
  void read( char* );
  void write( char* );
  std::string print();
  int by_name( std::string );

  bool pc_sat( bool );
  void addToPath( Expr * );

  bool subseteq( std::vector< Expr > *, std::vector< Expr > * );

  bool check_ide( std::vector< Expr > *, std::vector< Expr > * );
  int find( std::vector< std::vector< Expr > > *, char * );
  bool has( std::vector< std::vector< Expr > > *, char * );
  int addIfNew( std::vector< std::vector< Expr > > *, char * );
  void add( std::vector< std::vector< Expr > > *, char * );
};

}
#endif
